%!TEX root = forallxyyc.tex
\part{Dedução natural para LPO}%\part{Natural deduction for FOL}
\label{ch.NDFOL}
\addtocontents{toc}{\protect\mbox{}\protect\hrulefill\par}

\chapter{Regras básicas para LPO}\label{s:BasicFOL}%\chapter{Basic rules for FOL}\label{s:BasicFOL}

%The language of FOL makes use of all of the connectives of TFL. So proofs in FOL will use all of the basic and derived rules from Part~\ref{ch.NDTFL}. We will also use the proof-theoretic notions (particularly, the symbol `$\proves$') introduced there. However, we will also need some new basic rules to govern the quantifiers, and to govern the identity sign.

A linguagem da LPO faz uso de todos os conectivos da LVF. Então, provas na LPO vão seguir todas as regras básicas e derivadas da parte~\ref{ch.NDTFL}. Também usaremos as noções prova-teóricas (particularmente, o símbolo `$\proves$') introduzidas aqui. Contudo, também precisaremos de algumas novas regras básicas para governarem os quantificadores e os símbolos de identidade.


\section{Eliminação do universal}%\section{Universal elimination}

%From the claim that everything is~$F$, you can infer that any particular thing is~$F$. You name it; it's~$F$. So the following should be fine:
Da afirmação de que tudo é~$F$, você pode inferir que qualquer coisa particular é~$F$. Você a nomeia; ela é~$F$. Então, o seguinte deve raciocínio deve ser bom:
\begin{proof}
	\hypo{a}{\forall x\,\atom{R}{x,x,d}}
	\have{c}{\atom{R}{a,a,d}} \Ae{a}
\end{proof}
%We obtained line 2 by dropping the universal quantifier and replacing every instance of `$x$' with `$a$'. Equally, the following should be allowed:
Obtivemos a linha 2 ao eliminar o quantificador universal e substituir toda instância de `$x$' com `$a$'. Da mesma maneira, o seguinte deve ser permitido:
\begin{proof}
	\hypo{a}{\forall x\,\atom{R}{x,x,d}}
	\have{c}{\atom{R}{d,d,d}} \Ae{a}
\end{proof}
%We obtained line 2 here by dropping the universal quantifier and replacing every instance of `$x$' with `$d$'. We could have done the same with any other name we wanted. 
Obtivemos a linha 2 aqui eliminando o quantificador universal e subsituindo toda instância de `$x$' por `$d$'. Poderíamos ter feito o mesmo com qualquer outro nome que quiséssemos.

%This motivates the universal elimination rule ($\forall$E):
Isso motiva a regra da eliminação do universal (E$\forall$):
\factoidbox{
\begin{proof}
	\have[m]{a}{\forall \meta{x}\,\meta{A}(\ldots \meta{x} \ldots \meta{x}\ldots)}
	\have[\ ]{c}{\meta{A}(\ldots \meta{c} \ldots \meta{c}\ldots)} \Ae{a}
\end{proof}}
%The notation here was introduced in \S\ref{s:TruthFOL}. The point is that you can obtain any \emph{substitution instance} of a universally quantified formula: replace every instance of the quantified variable with any name you like. 
A notação aqui foi introduzida em \S\ref{s:TruthFOL}. O ponto é que você pode obter qualquer \emph{instância de substituição} de uma fórmula universalmente quantificada: substitua qualquer instância da variável quantificada com qualquer nome que você quiser.

%We should emphasize that (as with every elimination rule) you can only apply the $\forall$E rule when the universal quantifier is the main logical operator. So the following is \emph{banned}:
Devemos enfatizar que (como com toda regra de eliminação) você só pode aplicar a regra $E\forall$ quando o quantificador universal é o operador principal. Então, o seguinte é \emph{proibido}:
\begin{proof}
	\hypo{a}{\forall x\,\atom{B}{x} \eif \atom{B}{k}}
	%\have{c}{\atom{B}{b} \eif \atom{B}{k}}\by{naughy attempt to invoke $\forall$E}{a}
	\have{c}{\atom{B}{b} \eif \atom{B}{k}}\by{tentativa inadequada de invocar $\forall$E}{a}
\end{proof}
%This is illegitimate, since `$\forall x$' is not the main logical operator in line 1. (If you need a reminder as to why this sort of inference should be banned, reread \S\ref{s:MoreMonadic}.)
Isso é ilegítimo, uma vez que `$\forall x$' não é o operador lógico principal na linha 1. (Se você precisa de um lembrete sobre por que esse tipo de inferência deve ser proibida, releia \S\ref{s:MoreMonadic}.)

\section{Introdução do existencial}%\section{Existential introduction}
%From the claim that some particular thing is~$F$, you can infer that something is~$F$. So we ought to allow:
Da afirmação de que alguma coisa em particular é~$F$, você pode inferor que algo é~$F$. Então, devemos permitir:
\begin{proof}
	\hypo{a}{\atom{R}{a,a,d}}
	\have{b}{\exists x\, \atom{R}{a,a,x}} \Ei{a}
\end{proof}
%Here, we have replaced the name `$d$' with a variable `$x$', and then existentially quantified over it. Equally, we would have allowed:
Aqui, nós substituímos o nome `$d$' pela variável `$x$', e então quantificamos existencialmente sobre ela. Da mesma forma, permitiríamos:
\begin{proof}
	\hypo{a}{\atom{R}{a,a,d}}
	\have{c}{\exists x\, \atom{R}{x,x,d}} \Ei{a}
\end{proof}
%Here we have replaced both instances of the name `$a$' with a variable, and then existentially generalised. But we do not need to replace \emph{both} instances of a name with a variable: if Narcissus loves himself, then there is someone who loves Narcissus. So we also allow:
Aqui, nós substituímos ambas as instâncias do nome `$a$' por uma variável, e então generalizamos existencialmente. Mas nós não precisamos substituir \emph{ambas} as instâncias de um nome com uma variável: se Narcissus amava a si próprio, então há alguém que ama Narcissus. Então, nós também permitimos:
\begin{proof}
	\hypo{a}{\atom{R}{a,a,d}}
	\have{d}{\exists x\, \atom{R}{x,a,d}} \Ei{a}
\end{proof}
%Here we have replaced \emph{one} instance of the name `$a$' with a variable, and then existentially generalised. These observations motivate our introduction rule, although to explain it, we will need to introduce some new notation.
Aqui, substituímos \emph{uma} instância do nome `$a$' por uma variável, e então generalizamos existencialmente. Estas observações motivam nossa regra de introdução, apesar de que para explicá-la, precisaremos introduzir algumas notações novas.

%Where $\meta{A}$ is a sentence containing the name $\meta{c}$, we can emphasize this by writing `$\meta{A}(\ldots \meta{c} \ldots \meta{c}\ldots)$'. We will write `$\meta{A}(\ldots \meta{x} \ldots \meta{c}\ldots)$' to indicate any formula obtained by replacing \emph{some or all} of the instances of the name \meta{c} with the variable \meta{x}. Armed with this, our introduction rule is:
Onde $\meta{A}$ é uma sentença contendo o nome $\meta{c}$, podemos enfatizar isso ao escrever `$\meta{A}(\ldots \meta{c} \ldots \meta{c}\ldots)$'. Escreveremos `$\meta{A}(\ldots \meta{x} \ldots \meta{c}\ldots)$' para indicar qualquer fórmula obtida ao substituir \emph{alguma ou todas} das instâncias do nome \meta{c} pela variável \meta{x}. Armados com isso, nossa regra de introdução será:
\factoidbox{
\begin{proof}
	\have[m]{a}{\meta{A}(\ldots \meta{c} \ldots \meta{c}\ldots)}
	\have[\ ]{c}{\exists \meta{x}\,\meta{A}(\ldots \meta{x} \ldots \meta{c}\ldots)} \Ei{a}
\end{proof}
%\meta{x} must not occur in $\meta{A}(\ldots \meta{c} \ldots \meta{c}\ldots)$}
\meta{x} não pode ocorrer em $\meta{A}(\ldots \meta{c} \ldots \meta{c}\ldots)$}
%The constraint is included to guarantee that any application of the rule yields a  sentence of FOL. Thus the following is allowed:
A restrição é incluída para garantir que qualquer aplicação da regra produz uma sentença da LPO. Então, o seguinte é permitido:
\begin{proof}
	\hypo{a}{\atom{R}{a,a,d}}
	\have{d}{\exists x\, \atom{R}{x,a,d}} \Ei{a}
	\have{e}{\exists y \exists x\, \atom{R}{x,y,d}} \Ei{d}
\end{proof}
%But this is banned:
Mas isso é proibido:
\begin{proof}
	\hypo{a}{\atom{R}{a,a,d}}
	\have{d}{\exists x\, \atom{R}{x,a,d}} \Ei{a}
	%\have{e}{\exists x\, \exists x\, \atom{R}{x,x,d}}\by{naughty attempt to invoke $\exists$I}{d}
	\have{e}{\exists x\, \exists x\, \atom{R}{x,x,d}}\by{tentativa inadequada de invocar $\exists$I}{d}
\end{proof}
%since the expression on line~3 contains clashing variables, and so is not a sentence of FOL.
uma vez que a expressão na linha~3 contém variáveis conflitantes, e então não é uma sentença da LPO.

\section{Domínios vazios}%\section{Empty domains}
%The following proof combines our two new rules for quantifiers:
A prova seguinte combina nossas duas novas regras para quantificadores:
	\begin{proof}
		\hypo{a}{\forall x\, \atom{F}{x}}
		\have{in}{\atom{F}{a}}\Ae{a}
		\have{e}{\exists x\, \atom{F}{x}}\Ei{in}
	\end{proof}
%Could this be a bad proof? If anything exists at all, then certainly we can infer that something is~$F$, from the fact that everything is~$F$. But what if \emph{nothing} exists at all? Then it is surely vacuously true that everything is~$F$; however, it does not following that something is~$F$, for there is nothing to \emph{be}~$F$. So if we claim that, as a matter of logic alone, `$\exists x\,\atom{F}{x}$' follows from `$\forall x\,\atom{F}{x}$', then we are claiming that, as a matter of \emph{logic alone}, there is something rather than nothing. This might strike us as a bit odd.
Poderia esta ser uma prova ruim? Se algo existe, então certamente podemos inferir que algo é~$F$ do fato de que tudo é~$F$. Mas e se \emph{nada} existir? Então certamente é vacuosamente verdadeiro que tudo é~$F$; contudo, não se segue que algo é~$F$, porque não há nada para \emph{ser}~$F$. Então, se afirmarmos que, por uma questão puramente lógica, `$\exists x\,\atom{F}{x}$' se segue de `$\forall x\,\atom{F}{x}$', então, estaremos afirmando que, por uma questão \emph{puramente lógica}, há algo em vez de nada. Isso pode parecer um pouco estranho.

%Actually, we are already committed to this oddity. In \S\ref{s:FOLBuildingBlocks}, we stipulated that domains in FOL must have at least one member. We then defined a validity (of FOL) as a sentence which is true in every interpretation. Since `$\exists x\, x=x$' will be true in every interpretation, this \emph{also} had the effect of stipulating that it is a matter of logic that there is something rather than nothing.
Na verdade, já estamos comprometidos com essa estranheza. Em \S\ref{s:FOLBuildingBlocks}, estipulamos que domínios na LPO devem ter pelo menos um elemento. Nós então definimos uma tautologia (da LPO) como uma sentença que é verdadeira em toda interpretação. Uma vez que `$\exists x\, x=x$' será verdadeira em toda interpretação, isso \emph{também} tem o efeito de estipular que é uma questão lógica o fato de haver algo em vez de nada.

%Since it is far from clear that logic should tell us that there must be something rather than nothing, we might well be cheating a bit here. 
Uma vez que está longe de estar claro que a lógica deveria nos dizer que há algo em vez de nada, poderíamos muito bem estar trapaceando um pouco aqui.

%If we refuse to cheat, though, then we pay a high cost. Here are three things that we want to hold on to:
Se nos recusarmos a trapacear, porém, então pagaremos um alto preço. Aqui estão três coisas que gostaremos de manter:
	\begin{ebullet}
		\item $\forall x\,\atom{F}{x} \proves \atom{F}{a}$: afinal, isso é $\forall$E.%after all, that was $\forall$E.
		\item $\atom{F}{a} \proves \exists x\,\atom{F}{x}$: Afinal, isso é $\exists$I.%after all, that was $\exists$I.
		%\item the ability to copy-and-paste proofs together: after all, reasoning works by putting lots of little steps together into rather big chains.
		\item a habilidade de copiar e colar provas juntas: afinal, o raciocínio funciona colocando vários pequenos passos juntos em grandes cadeias.
	\end{ebullet}
%If we get what we want on all three counts, then we have to countenance that $\forall xFx \proves \exists x\,\atom{F}{x}$. So, if we get what we want on all three counts, the proof system alone tells us that there is something rather than nothing. And if we refuse to accept that, then we have to surrender one of the three things that we want to hold on to!
Se obtivermos o que queremos em todos os três pontos, então teremos que admitir que $\forall xFx \proves \exists x\,\atom{F}{x}$. Então, se obtivermos o que queremos em todos os três pontos, o sistema de prova sozinho nos mostra que há algo em vez de nada. E se nos recusarmos a aceitar isso, então teremos que renunciar a uma das três coisas que nós queremos manter!

%Before we start thinking about which to surrender, we might want to ask how \emph{much} of a cheat this is. Granted, it may make it harder to engage in theological debates about why there is something rather than nothing. But the rest of the time, we will get along just fine. So maybe we should just regard our proof system (and FOL, more generally) as having a very slightly limited purview. If we ever want to allow for the possibility of \emph{nothing}, then we will have to cast around for a more complicated proof system. But for as long as we are content to ignore that possibility, our proof system is perfectly in order. (As, similarly, is the stipulation that every domain must contain at least one object.)
Antes de começarmos a pensar sobre o que renunciar, podemos perguntar o quanto isso é uma trapaça. Admitido, isso pode dificultar o debate teológico sobre por que há algo em vez de nada. Mas no resto do tempo, nos daremos bem. Então, talvez devêssemos considerar nosso sistema de provas (e a LPO, de maneira mais geral) como tendo um alcance muito limitado. Se quisermos permitir a possibilidade de \emph{nada}, teremos que procurar um sistema de provas mais complicado. Mas enquanto nos contentarmos em ignorar essa possibilidade, nosso sistema de provas estará perfeitamente em ordem. (Como, da mesma forma, é a estipulação de que todo domínio deve conter pelo menos um objeto).


\section{Introdução do universal}%\section{Universal introduction}
%Suppose you had shown of each particular thing that it is F (and that there are no other things to consider). Then you would be justified in claiming that everything is F. This would motivate the following proof rule. If you had established each and every single substitution instance of `$\forall x\,\atom{F}{x}$', then you can infer `$\forall x\,\atom{F}{x}$'. 
Suponha que você mostrou, sobre cada coisa particular, que ela é F (e que não há outras coisas para considerar). Então, você estaria justificado em afirmar que tudo é F. Isso motivaria a seguinte regra de prova. Se você estabeleceu todas as instâncias de substituição de `$\forall x\,\atom{F}{x}$', então você pode inferir `$\forall x\,\atom{F}{x}$'. 

%Unfortunately, that rule would be utterly unusable. To establish each and every single substitution instance would require proving `$\atom{F}{a}$', `$\atom{F}{b}$', \dots, `$\atom{F}{j_2}$', \dots, `$\atom{F}{r_{79002}}$', \ldots, and so on. Indeed, since there are infinitely many names in FOL, this process would never come to an end. So we could never apply that rule. We need to be a bit more cunning in coming up with our rule for introducing universal quantification. 
Infelizmente, esta regra seria totalmente inutilizável. Estabelecer que instância de substituição requereria provar `$\atom{F}{a}$', `$\atom{F}{b}$', \dots, `$\atom{F}{j_2}$', \dots, `$\atom{F}{r_{79002}}$', \ldots, e assim por diante. De fato, uma vez que há infinitos nomes na LPO, esse processo nunca terminaria. Então, nunca poderíamos aplicar esta regra. Precisamos ser um pouco mais astutos ao criar nossa regra para introduzir o quantificador universal.

%A solution will be inspired by considering:
Uma solução será inspirada ao se considerar:
$$\forall x\,\atom{F}{x} \therefore \forall y\,\atom{F}{y}$$
%This argument should \emph{obviously} be valid. After all, alphabetical variation ought to be a matter of taste, and of no logical consequence. But how might our proof system reflect this? Suppose we begin a proof thus:
Este argumento deve \emph{obviamente} ser falso. Afinal, a variação alfabética deve ser uma questão de gosto, e sem qualquer consequência lógica. Mas como nosso sistema de prova poderia refletir isso? Suponha que começamos uma prova assim:
\begin{proof}
	\hypo{x}{\forall x\, \atom{F}{x}} 
	\have{a}{\atom{F}{a}} \Ae{x}
\end{proof}
%We have proved `$\atom{F}{a}$'. And, of course, nothing stops us from using the same justification to prove `$\atom{F}{b}$', `$\atom{F}{c}$', \ldots, `$\atom{F}{j_2}$', \ldots, `$\atom{F}{r_{79002}}$, \dots, and so on until we run out of space, time, or patience. But reflecting on this, we see that there is a way to prove $F\meta{c}$, for any name \meta{c}. And if we can do it for \emph{any} thing, we should surely be able to say that `$F$' is true of \emph{everything}. This therefore justifies us in inferring `$\forall y\,\atom{F}{y}$', thus:
Nós provamos `$\atom{F}{a}$'. E, é claro, nada nos impede de usar a mesma justificação para provar `$\atom{F}{b}$', `$\atom{F}{c}$', \ldots, `$\atom{F}{j_2}$', \ldots, `$\atom{F}{r_{79002}}$, \dots, e assim por diante, até ficarmos sem espaço, tempo ou paciência. Mas, refletindo sobre isso, nós vemos que há uma forma de provar $F\meta{c}$, para qualquer nome \meta{c}. E, se podemos fazer isso para \emph{qualquer} qualquer coisa, então certamente podemos dizer que `$F$' é verdadeiro sobre \emph{tudo}. Portanto, isso nos justifica em inferir `$\forall y\,\atom{F}{y}$', assim:
\begin{proof}
	\hypo{x}{\forall x\, \atom{F}{x}}
	\have{a}{\atom{F}{a}} \Ae{x}
	\have{y}{\forall y\, \atom{F}{y}} \Ai{a}
\end{proof}
%The crucial thought here is that `$a$' was just some \emph{arbitrary} name. There was nothing special about it---we might have chosen any other name---and still the proof would be fine. And this crucial thought motivates the universal introduction rule ($\forall$I):
O pensamento crucial aqui é que `$a$' era apenas algum nome \emph{arbitrário}. Não havia nada de especial sobre ele---poderíamos ter escolhido qualquer outro nome---e a prova ainda continuaria correta. E este pensamento crucial motiva a regra da introdução do universal ($\forall$I).
\factoidbox{
\begin{proof}
	\have[m]{a}{\meta{A}(\ldots \meta{c} \ldots \meta{c}\ldots)}
	\have[\ ]{c}{\forall \meta{x}\,\meta{A}(\ldots \meta{x} \ldots \meta{x}\ldots)} \Ai{a}
\end{proof}
	\meta{c} não pode ocorrer em nenhuma assunção não eliminada%must not occur in any undischarged assumption\\ 
	\meta{x} não pode ocorrer em $\meta{A}(\ldots \meta{c} \ldots \meta{c}\ldots)$}%must not occur in $\meta{A}(\ldots \meta{c} \ldots \meta{c}\ldots)$}
%A crucial aspect of this rule, though, is bound up in the first constraint. This constraint ensures that we are always reasoning at a sufficiently general level.
Um aspecto crucial dessa regra, porém, está associado à primeira restrição. Esta restrição garante que estamos sempre raciocinando em um nível suficientemente geral.
%\footnote{Recall from \S\ref{s:BasicTFL} that we are treating `$\ered$' as a canonical contradiction. But if it were the canonical contradiction as involving some \emph{constant}, it might interfere with the constraint mentioned here. To avoid such problems, we will treat `$\ered$' as a canonical contradiction \emph{that involves no particular names}.} 
%To see the constraint in action, consider this terrible argument:
Para ver a restrição em ação, considere este terrível argumento:
	\begin{quote}
		Todos amam Kylie Minogue; portanto, todos amam a si mesmos.%Everyone loves Kylie Minogue; therefore everyone loves themselves.
	\end{quote}
%We might symbolize this obviously invalid inference pattern as:
Poderíamos simbolizar este padrão de inferência obviamente inválido como:
$$\forall x\,\atom{L}{x,k} \therefore \forall x\,\atom{L}{x,x}$$
%Now, suppose we tried to offer a proof that vindicates this argument:
Agora, suponha que nós tentamos oferecer uma prova que justifique esse argumento:
\begin{proof}
	\hypo{x}{\forall x\, \atom{L}{x,k}}
	\have{a}{\atom{L}{k,k}} \Ae{x}
	\have{y}{\forall x\, \atom{L}{x,x}} \by{tentativa inadequada de invocar $\forall$I}{a}%\by{naughty attempt to invoke $\forall$I}{a}
\end{proof}\noindent
%This is not allowed, because `$k$' occurred already in an undischarged assumption, namely, on line 1. The crucial point is that, if we have made any assumptions about the object we are working with, then we are not reasoning generally enough to license $\forall$I.
Isso não é permitido, porque `$k$' já ocorreu em uma assunção não eliminada, a saber, a da linha 1. O ponto crucial é que, se fizermos qualquer assunção sobre o objeto com o qual estamos trabalhando, então não estamos raciocinando de maneira geral o suficiente para permitimos o uso de $\forall$I.

%Although the name may not occur in any \emph{undischarged} assumption, it may occur in a \emph{discharged} assumption. That is, it may occur in a subproof that we have already closed. For example, this is just fine:
Apesar de o nome não poder ocorrer em qualquer assunção \emph{não eliminada}, ele pode ocorrer em uma assunção \emph{eliminada}. Ou seja, ele pode ocorrer em uma subprova que já fechamos. Por exemplo, isso está correto:
\begin{proof}
	\open
		\hypo{f1}{\atom{G}{d}}
		\have{f2}{\atom{G}{d}}\by{R}{f1}
	\close
	\have{ff}{\atom{G}{d} \eif \atom{G}{d}}\ci{f1-f2}
	\have{zz}{\forall z(\atom{G}{z} \eif \atom{G}{z})}\Ai{ff}
\end{proof}
%This tells us that `$\forall z (\atom{G}{z} \eif \atom{G}{z})$' is a \emph{theorem}. And that is as it should be.
Isso nos diz que `$\forall z (\atom{G}{z} \eif \atom{G}{z})$' é um \emph{teorema}. E isso é como deve ser.

%We should emphasise one last point. As per the conventions of \S\ref{s:MainLogicalOperatorQuantifier}, the use of $\forall$I requires that we are replacing \emph{every} instance of the name \meta{c} in $\meta{A}(\ldots \meta{x}\ldots\meta{x}\ldots)$ with the variable \meta{x}. If we only replace \emph{some} names and not others, we end up `proving' silly things. For example, consider the argument:
Devemos enfatizar um último ponto. Conforme as convenções de \S\ref{s:MainLogicalOperatorQuantifier}, o uso de $\forall$I requer que nós substituamos \emph{toda} instância do nome \meta{c} em $\meta{A}(\ldots \meta{x}\ldots\meta{x}\ldots)$ com a variável \meta{x}. Se apenas substituirmos \emph{alguns} nomes e não outros, acabaremos `provando' coisas bem estranhas. Por exemplo, considere o argumento:
	\begin{quote}
	%Everyone is as old as themselves; so everyone is as old as Judi Dench
	Todo mundo é tão velho quanto a si mesmo; então, todos são tão velhos quanto Judi Dench
	\end{quote}
Podemos simbolizar isso assim:%We might symbolise this as follows:
$$\forall x\,\atom{O}{x,x} \therefore \forall x\,\atom{O}{x,d}$$
%But now suppose we tried to \emph{vindicate} this terrible argument with the following:
Mas, agora, sponha que tentamos \emph{justificar} este terrível argumento com o seguinte:
\begin{proof}
	\hypo{x}{\forall x\, \atom{O}{x,x}}
	\have{a}{\atom{O}{d,d}}\Ae{x}
	\have{y}{\forall x\, \atom{O}{x,d}}\by{tentativa inadequada de invocar $\forall$I}{a}	
%\end{proof}%\by{naughty attempt to invoke $\forall$I}{a}	
\end{proof}
%Fortunately, our rules do not allow for us to do this: the attempted proof is banned, since it doesn't replace \emph{every} occurrence of `$d$' in line $2$ with an `$x$'.
Felizmente, nossas regras não nos permitem fazer isso: a tentativa de prova é proibida, uma vez que ela não substitui \emph{todas} as ocorrências de `$d$' na linha $2$ com um `$x$'.

\section{Eliminação do existencial}%\section{Existential elimination}
%Suppose we know that \emph{something} is~$F$. The problem is that simply knowing this does not tell us which thing is~$F$. So it would seem that from `$\exists x\,\atom{F}{x}$' we cannot immediately conclude `$\atom{F}{a}$', `$\atom{F}{e_{23}}$', or any other substitution instance of the sentence. What can we do?
Suponha que sabemos que \emph{algo} é~$F$. O problema é que simplesmente saber isso não nos diz qual coisa é~$F$. Então, pareceria que de `$\exists x\,\atom{F}{x}$' nós não podemos concluir imediatamente que `$\atom{F}{a}$', `$\atom{F}{e_{23}}$', ou qualquer outra instância de substituição da sentença. O que podemos fazer?

%Suppose we know that something is~$F$, and that everything which is~$F$ is also~$G$. In (almost) natural English, we might reason thus:
Suponha que nós sabemos que algo é~$F$, e que tudo que é~$F$ também é~$G$. No português (quase) natural, nós poderíamos racionar assim:
	\begin{quote}
		%Since something is $F$, there is some particular thing which is an~$F$. We do not know anything about it, other than that it's an~$F$, but for convenience, let's call it `Becky'. So: Becky is $F$. Since everything which is $F$ is~$G$, it follows that Becky is~$G$. But since Becky is~$G$, it follows that something is~$G$. And nothing depended on which object, exactly, Becky was. So, something is~$G$.
		Uma vez que algo é $F$, há uma coisa particular que é um~$F$. Nós não sabemos qualquer coisa sobre ela, além do fato de que ela é um~$F$, mas, por conveniência, vamos chamá-la de `Becky'. Então Becky é $F$. Uma vez que tudo que é $F$ é~$G$, segue-se que Becky é~$G$. Mas, uma vez que Becky é~$G$, segue-se que algo é~$G$. E nada dependeu de qual objeto, exatamente, Becky foi. Então, algo é~$G$.
	\end{quote}
%We might try to capture this reasoning pattern in a proof as follows:
Poderíamos tentar capturar este padrão de raciocínio em uma prova como se segue:
\begin{proof}
	\hypo{es}{\exists x\, \atom{F}{x}}
	\hypo{ast}{\forall x(\atom{F}{x} \eif \atom{G}{x})}
	\open
		\hypo{s}{\atom{F}{b}}
		\have{st}{\atom{F}{b} \eif \atom{G}{b}}\Ae{ast}
		\have{t}{\atom{G}{b}} \ce{st, s}
		\have{et1}{\exists x\, \atom{G}{x}}\Ei{t}
	\close
	\have{et2}{\exists x\, \atom{G}{x}}\Ee{es,s-et1}
\end{proof}\noindent
%Breaking this down: we started by writing down our assumptions. At line~$3$, we made an additional assumption: `$\atom{F}{b}$'. This was just a substitution instance of `$\exists x\,\atom{F}{x}$'. On this assumption, we established `$\exists x\,\atom{G}{x}$'. Note that we had made no \emph{special} assumptions about the object named by `$b$'; we had \emph{only} assumed that it satisfies `$\atom{F}{x}$'. So nothing depends upon which object it is. And line~$1$ told us that \emph{something} satisfies `$\atom{F}{x}$', so our reasoning pattern was perfectly general. We can discharge the specific assumption `$\atom{F}{b}$', and simply infer `$\exists x\,\atom{G}{x}$' on its own.
Desconstruindo isso: nós começamos ao escrever nossas assunções. Na linha~$3$, fizemos uma assunção adicional: `$\atom{F}{b}$'. Esta foi apenas uma instância de substituição de `$\exists x\,\atom{F}{x}$'. Sobre esta assunção, nós estabelecemos `$\exists x\,\atom{G}{x}$'. Note que não fizemos qualquer assunção \emph{especial} sobre o objeto nomeado por `$b$'; nós \emph{apenas} assumimos que ele satisfaz `$\atom{F}{x}$'. Então, nada depende de qual objeto ele é. E a linha~$1$ nos diz que \emph{algo} satisfaz `$\atom{F}{x}$', então, nosso padrão de raciocínio foi perfeitamente geral. Podemos eliminar a assunção específica `$\atom{F}{b}$', e simplesmente inferir `$\exists x\,\atom{G}{x}$' sozinha.


%Putting this together, we obtain the existential elimination rule ($\exists$E):
Juntando tudo, obtemos a regra da eliminação do existencial ($\exists$E):
\factoidbox{
\begin{proof}
	\have[m]{a}{\exists \meta{x}\,\meta{A}(\ldots \meta{x} \ldots \meta{x}\ldots)}
	\open	
		\hypo[i]{b}{\meta{A}(\ldots \meta{c} \ldots \meta{c}\ldots)}
		\have[j]{c}{\meta{B}}
	\close
	\have[\ ]{d}{\meta{B}} \Ee{a,b-c}
\end{proof}
\meta{c} não pode ocorrer em qualquer assunção não eliminada antes da linha $i$\\%must not occur in any assumption undischarged before line $i$\\
\meta{c} não pode ocorrer em $\exists \meta{x}\,\meta{A}(\ldots \meta{x} \ldots \meta{x}\ldots)$\\%must not occur in $\exists \meta{x}\,\meta{A}(\ldots \meta{x} \ldots \meta{x}\ldots)$\\
\meta{c} não pode ocorrer em \meta{B}}%must not occur in \meta{B}}
%As with universal introduction, the constraints are extremely important. To see why, consider the following terrible argument:
Como na introdução do universal, as restrições são extremamente importantes. Para ver o porquê, considere o terrível argumento a seguir:
	\begin{quote}
		%Tim Button is a lecturer. Someone is not a lecturer. So Tim Button is both a lecturer and not a lecturer.
		Tim Button é um palestrante. Alguém não é um palestrante. Então, Tim Button é e não é um palestrante.
	\end{quote}
%We might symbolize this obviously invalid inference pattern as follows:
Poderíamos simbolizar este padrão de inferência obviamente inválido como se segue:
$$\atom{L}{b}, \exists x\, \enot\atom{L}{x} \therefore \atom{L}{b} \eand \enot \atom{L}{b}$$
%Now, suppose we tried to offer a proof that vindicates this argument:
Agora, suponha que tentamos oferecer uma prova que justifique o argumento:
\begin{proof}
	\hypo{f}{\atom{L}{b}}
	\hypo{nf}{\exists x\, \enot \atom{L}{x}}	
	\open	
		\hypo{na}{\enot \atom{L}{b}}
		\have{con}{\atom{L}{b} \eand \enot \atom{L}{b}}\ai{f, na}
	\close
	\have{econ1}{\atom{L}{b} \eand \enot \atom{L}{b}}\by{naughty attempt}{}
	\have[\ ]{x}{}\by{to invoke $\exists$E }{nf, na-con}
\end{proof}
%The last line of the proof is not allowed. The name that we used in our substitution instance for `$\exists x\, \enot \atom{L}{x}$' on line~$3$, namely `$b$', occurs in line~$4$. The this would be no better:
A última linha da prova não é permitida. O nome que usamos em nossa instância de substituição para `$\exists x\, \enot \atom{L}{x}$' na linha~$3$, a saber, `$b$', ocorre na linha~$4$. Isso não seria melhor:

\begin{proof}
	\hypo{f}{\atom{L}{b}}
	\hypo{nf}{\exists x\, \enot \atom{L}{x}}	
	\open	
		\hypo{na}{\enot \atom{L}{b}}
		\have{con}{\atom{L}{b} \eand \enot \atom{L}{b}}\ai{f, na}
		\have{con1}{\exists x (\atom{L}{x} \eand \enot \atom{L}{x})}\Ei{con}		
	\close
	%\have{econ1}{\exists x (\atom{L}{x} \eand \enot \atom{L}{x})}\by{naughty attempt}{}
	\have{econ1}{\exists x (\atom{L}{x} \eand \enot \atom{L}{x})}\by{tentativa inadequada}{}
	\have[\ ]{x}{}\by{to invoke $\exists$E }{nf, na-con1}
\end{proof}
%The last line is still not allowed. For the name that we used in our substitution instance for `$\exists x\, \enot \atom{L}{x}$', namely `$b$', occurs in an undischarged assumption, namely line~$1$. 
A última linha ainda não é permitida. Pois, o nome que usamos em nossa instância de subsituição de `$\exists x\, \enot \atom{L}{x}$', a saber, `$b$', ocorre em uma assunção não eliminada, a saber, a linha~$1$.

%The moral of the story is this. \emph{If you want to squeeze information out of an existential quantifier, choose a new name for your substitution instance.} That way, you can guarantee that you meet all the constraints on the rule for $\exists$E.
A moral da história é esta. \emph{Se você quiser extrair informações de um quantificador existencial, escolha um novo nome para sua instância de substituição.} Dessa forma, você pode garantir que você vai cumprir todas as restrições da regra para $\exists$E.

\practiceproblems
\problempart
%Explain why these two `proofs' are \emph{incorrect}. Also, provide interpretations which would invalidate the fallacious argument forms the `proofs' enshrine:
Explique por que essas duas `provas' estão \emph{incorretas}. Ainda, forneça interpretações que invalidariam o argumento falacioso que as provas consagram:
\begin{multicols}{2}
	\begin{proof}
		\hypo{Rxx}{\forall x\, \atom{R}{x,x}}
		\have{Raa}{\atom{R}{a,a}}\Ae{Rxx}
		\have{Ray}{\forall y\, \atom{R}{a,y}}\Ai{Raa}
		\have{Rxy}{\forall x\, \forall y\, \atom{R}{x,y}}\Ai{Ray}
	\end{proof}
	\begin{proof}
		\hypo{AE}{\forall x\, \exists y\, \atom{R}{x,y}}
		\have{E}{\exists y\, \atom{R}{a,y}}\Ae{AE}
		\open
			\hypo{ass}{\atom{R}{a,a}}
			\have{Ex}{\exists x\, \atom{R}{x,x}}\Ei{ass}
		\close
		\have{con}{\exists x\, \atom{R}{x,x}}\Ee{E, ass-Ex}
	\end{proof}
\end{multicols}

\problempart 
\label{pr.justifyFOLproof}
%The following three proofs are missing their citations (rule and line numbers). Add them, to turn them into bona fide proofs. 
Nas seguintes três provas faltam as citações (regra e número das linhas). Adicione-as, para torná-las provas genuínas.
\begin{earg}
\item \begin{proof}
\hypo{p1}{\forall x\exists y(\atom{R}{x,y} \eor \atom{R}{y,x})}
\hypo{p2}{\forall x\,\enot \atom{R}{m,x}}
\have{3}{\exists y(\atom{R}{m,y} \eor \atom{R}{y,m})}{}
	\open
		\hypo{a1}{\atom{R}{m,a} \eor \atom{R}{a,m}}
		\have{a2}{\enot \atom{R}{m,a}}{}
		\have{a3}{\atom{R}{a,m}}{}
		\have{a4}{\exists x\, \atom{R}{x,m}}{}
	\close
\have{n}{\exists x\, \atom{R}{x,m}} {}
\end{proof}

\item \begin{proof}
\hypo{1}{\forall x(\exists y\,\atom{L}{x,y} \eif \forall z\,\atom{L}{z,x})}
\hypo{2}{\atom{L}{a,b}}
\have{3}{\exists y\,\atom{L}{a,y} \eif \forall z\atom{L}{z,a}}{}
\have{4}{\exists y\, \atom{L}{a,y}} {}
\have{5}{\forall z\, \atom{L}{z,a}} {}
\have{6}{\atom{L}{c,a}}{}
\have{7}{\exists y\,\atom{L}{c,y} \eif \forall z\,\atom{L}{z,c}}{}
\have{8}{\exists y\, \atom{L}{c,y}}{}
\have{9}{\forall z\, \atom{L}{z,c}}{}
\have{10}{\atom{L}{c,c}}{}
\have{11}{\forall x\, \atom{L}{x,x}}{}
\end{proof}

\item \begin{proof}
\hypo{a}{\forall x(\atom{J}{x} \eif \atom{K}{x})}
\hypo{b}{\exists x\,\forall y\, \atom{L}{x,y}}
\hypo{c}{\forall x\, \atom{J}{x}}
\open
	\hypo{2}{\forall y\, \atom{L}{a,y}}
	\have{3}{\atom{L}{a,a}}{}
	\have{d}{\atom{J}{a}}{}
	\have{e}{\atom{J}{a} \eif \atom{K}{a}}{}
	\have{f}{\atom{K}{a}}{}
	\have{4}{\atom{K}{a} \eand \atom{L}{a,a}}{}
	\have{5}{\exists x(\atom{K}{x} \eand \atom{L}{x,x})}{}
\close
\have{j}{\exists x(\atom{K}{x} \eand \atom{L}{x,x})}{}
\end{proof}
\end{earg}

\problempart
\label{pr.BarbaraEtc.proof1}
%In \S\ref{s:MoreMonadic} problem A, we considered fifteen syllogistic figures of Aristotelian logic. Provide proofs for each of the argument forms. NB: You will find it \emph{much} easier if you symbolize (for example) `No F is G' as `$\forall x (\atom{F}{x} \eif \enot \atom{G}{x})$'.
Em \S\ref{s:MoreMonadic}, problema A, consideramos quinze figuras silogísticas da lógica aristotélica. Forneça provas para cada uma das formas de argumento. Note: Você achará \emph{muito} mais fácil se você simbolizar (por exemplo) `Nenhum F é G' como `$\forall x (\atom{F}{x} \eif \enot \atom{G}{x})$'.

\

\problempart
\label{pr.BarbaraEtc.proof2}
%Aristotle and his successors identified other syllogistic forms which depended upon `existential import'. Symbolize each of these argument forms in FOL and offer proofs.
Aristóteles e seus sucessores identificaram outras formas silogísticas que dependem do `importe existencial'. Simbolize cada uma dessas formas de argumento na LPO e ofereça provas.
\begin{earg}
	%\item \textbf{Barbari.} Something is H. All G are F. All H are G. So: Some H is F
	%\item \textbf{Celaront.} Something is H. No G are F. All H are G. So: Some H is not F
	%\item \textbf{Cesaro.} Something is H. No F are G. All H are G. So: Some H is not F.
	%\item \textbf{Camestros.} Something is H. All F are G. No H are G. So: Some H is not F.
	%\item \textbf{Felapton.} Something is G. No G are F. All G are H. So: Some H is not F.
	%\item \textbf{Darapti.} Something is G. All G are F. All G are H. So: Some H is F.
	%\item \textbf{Calemos.} Something is H. All F are G. No G are H. So: Some H is not F.
	%\item \textbf{Fesapo.} Something is G. No F is G. All G are H. So: Some H is not F.
	%\item \textbf{Bamalip.} Something is F. All F are G. All G are H. So: Some H are F.
	
	\item \textbf{Barbari.} Algo é H. Todo G é F. Todo H é G. Então: Algum H é F
	\item \textbf{Celaront.} Algo é H. No G é F. Todo H é G. Então: Algum H não é F
	\item \textbf{Cesaro.} Algo é H. No F é G. Todo H é G. Então: Algum H não é F.
	\item \textbf{Camestros.} Algo é H. Todo F é G. No H é G. Então: Algum H não é F.
	\item \textbf{Felapton.} Algo é G. No G é F. Todo G é H. Então: Algum H não é F.
	\item \textbf{Darapti.} Algo é G. Todo G é F. Todo G é H. Então: Algum H é F.
	\item \textbf{Calemos.} Algo é H. Todo F é G. No G é H. Então: Algum H não é F.
	\item \textbf{Fesapo.} Algo é G. No F é G. Todo G é H. Então: Algum H não é F.
	\item \textbf{Bamalip.} Algo é F. Todo F é G. Todo G é H. Então: Algum H é F.
\end{earg}

\problempart
\label{pr.someFOLproofs}
Forneça uma prova de cada caso.%Provide a proof of each claim.
\begin{earg}
\item $\proves \forall x\,\atom{F}{x} \eif \forall y(\atom{F}{y} \eand \atom{F}{y})$
\item $\forall x(\atom{A}{x}\eif \atom{B}{x}), \exists x\,\atom{A}{x} \proves \exists x\,\atom{B}{x}$
\item $\forall x(\atom{M}{x} \eiff \atom{N}{x}), \atom{M}{a} \eand \exists x\,\atom{R}{x,a} \proves \exists x\,\atom{N}{x}$
\item $\forall x\, \forall y\,\atom{G}{x,y}\proves\exists x\,\atom{G}{x,x}$
\item $\proves\forall x\,\atom{R}{x,x} \eif \exists x\, \exists y\,\atom{R}{x,y}$
\item $\proves\forall y\, \exists x (\atom{Q}{y} \eif \atom{Q}{x})$
\item $\atom{N}{a} \eif \forall x(\atom{M}{x} \eiff \atom{M}{a}), \atom{M}{a}, \enot\atom{M}{b}\proves \enot \atom{N}{a}$
\item $\forall x\, \forall y (\atom{G}{x,y} \eif \atom{G}{y,x}) \proves \forall x\forall y (\atom{G}{x,y} \eiff \atom{G}{y,x})$
\item $\forall x(\enot\atom{M}{x} \eor \atom{L}{j,x}), \forall x(\atom{B}{x}\eif \atom{L}{j,x}), \forall x(\atom{M}{x}\eor \atom{B}{x})\proves \forall x\atom{L}{j,x}$
\end{earg}

\solutions
\problempart
\label{pr.likes}
%Write a symbolization key for the following argument, symbolize it, and prove it:
Escreva uma chave de simbolização para o seguinte argumento, simbolize-o e prove-o:
\begin{quote}
%There is someone who likes everyone who likes everyone that she likes. Therefore, there is someone who likes herself.
Há alguém que gosta de todos que gostam de todos que ela gosta. Portanto, há alguém que gosta de si mesmo.
\end{quote}


\problempart
%Show that each pair of sentences is provably equivalent.
Mostre que cada par de sentenças é comprovavelmente equivalente
\begin{earg}
\item $\forall x (\atom{A}{x}\eif \enot \atom{B}{x})$, $\enot\exists x(\atom{A}{x} \eand \atom{B}{x})$
\item $\forall x (\enot\atom{A}{x}\eif \atom{B}{d})$, $\forall x\,\atom{A}{x} \eor \atom{B}{d}$
\item $\exists x\,\atom{P}{x} \eif \atom{Q}{c}$, $\forall x (\atom{P}{x} \eif \atom{Q}{c})$
\end{earg}

\solutions
\problempart
\label{pr.FOLequivornot}
%For each of the following pairs of sentences: If they are provably equivalent, give proofs to show this. If they are not, construct an interpretation to show that they are not logically equivalent.
Para cada um dos seguintes pares de frases: Se forem comprovadamente equivalentes, dê provas para mostrar isso. Se não forem, construa uma interpretação para mostrar que eles não são logicamente equivalentes.

\begin{earg}
\item $\forall x\,\atom{P}{x} \eif \atom{Q}{c}, \forall x (\atom{P}{x} \eif \atom{Q}{c})$
\item $\forall x\,\forall y\, \forall z\,\atom{B}{x,y,z}, \forall x\,\atom{B}{x,x}x$
\item $\forall x\,\forall y\,\atom{D}{x,y}, \forall y\,\forall x\,\atom{D}{x,y}$
\item $\exists x\,\forall y\,\atom{D}{x,y}, \forall y\,\exists x\,\atom{D}{x,y}$
\item $\forall x (\atom{R}{c,a} \eiff \atom{R}{x,a}), \atom{R}{c,a} \eiff \forall x\,\atom{R}{x,a}$
\end{earg}

\solutions
\problempart
\label{pr.FOLvalidornot}
%For each of the following arguments: If it is valid in FOL, give a proof. If it is invalid, construct an interpretation to show that it is invalid.
Para cada um dos seguintes argumentos: Se for válido no FOL, forneça uma prova. Se for inválido, construa uma interpretação para mostrar que ele é inválido.

\begin{earg}
\item $\exists y\,\forall x\,\atom{R}{x,y} \therefore \forall x\,\exists y\,\atom{R}{x,y}$
\item $\forall x\,\exists y\,\atom{R}{x,y} \therefore  \exists y\,\forall x\,\atom{R}{x,y}$
\item $\exists x(\atom{P}{x} \eand \enot \atom{Q}{x}) \therefore \forall x(\atom{P}{x} \eif \enot \atom{Q}{x})$
\item $\forall x(\atom{S}{x} \eif \atom{T}{a}), \atom{S}{d} \therefore \atom{T}{a}$
\item $\forall x(\atom{A}{x}\eif \atom{B}{x}), \forall x(\atom{B}{x} \eif \atom{C}{x}) \therefore \forall x(\atom{A}{x} \eif \atom{C}{x})$
\item $\exists x(\atom{D}{x} \eor \atom{E}{x}), \forall x(\atom{D}{x} \eif \atom{F}{x}) \therefore \exists x(\atom{D}{x} \eand \atom{F}{x})$
\item $\forall x\,\forall y(\atom{R}{x,y} \eor \atom{R}{y,x}) \therefore \atom{R}{j,j}$
\item $\exists x\,\exists y(\atom{R}{x,y} \eor \atom{R}{y,x}) \therefore \atom{R}{j,j}$
\item $\forall x\,\atom{P}{x} \eif \forall x\,\atom{Q}{x}, \exists x\, \enot\atom{P}{x} \therefore \exists x\, \enot \atom{Q}{x}$
\item $\exists x\,\atom{M}{x} \eif \exists x\,\atom{N}{x}$, $\enot \exists x\,\atom{N}{x}\therefore  \forall x\, \enot \atom{M}{x}$
\end{earg}

\chapter{Provas com quantificadores}%\chapter{Proofs with quantifiers}

%In \S\ref{s:stratTFL} we discussed strategies for constructing proofs using the basic rules of natural deduction for TFL. The same principles apply to the rules for the quantifiers. If we want to prove a quantifier sentence $\forall \meta{x}\, \atom{\meta{A}}{\meta{x}}$ or $\exists \meta{x}\, \atom{\meta{A}}{\meta{x}}$. We can work backward by justifying the sentence we want by $\forall$I or $\exists$I and trying to find a proof of the corresponding premise of that rule. And to work forward from a quantified sentence, we apply $\forall$E or $\exists$E, as the case may be. 
%
Em \S\ref{s:stratTFL}, discutimos estratégias para construir provas usando as regras básicas da dedução natural para a LVF. Os mesmos princípios se aplicam às regras para quantificadores. Se quisermos provar uma sentença $\forall \meta{x}\, \atom{\meta{A}}{\meta{x}}$ ou $\exists \meta{x}\, \atom{\meta{A}}{\meta{x}}$, podemos trabalhar no sentido contrário justificando a sentença que queremos com $\forall$I ou $\exists$I e tentando encontrar uma prova da premissa correspondente daquela regra. E, para avançar a partir de uma sentença quantificada, aplicamos $\forall$E ou $\exists$E, conforme o caso.

%Specifically, suppose you want to prove $\forall \meta{x}\, \atom{\meta{A}}{\meta{x}}$. To do so using $\forall$I, we would need a proof of $\atom{\meta{A}}{\meta{c}}$ for some name~$\meta{c}$ which does not occur in any undischarged assumption. To apply the corresponding strategy, i.e., to construct a proof of $\forall \meta{x}\, \atom{\meta{A}}{\meta{x}}$ by working backward, is thus to write $\atom{\meta{A}}{\meta{c}}$ above it and then to continue to try to find a proof of that sentence.
%
Especificamente, suponha que você quer provar $\forall \meta{x}\, \atom{\meta{A}}{\meta{x}}$. Para fazer isso usando $\forall$I, precisaremos de uma prova de $\atom{\meta{A}}{\meta{c}}$ para algum nome~$\meta{c}$ que não ocorre em qualquer assunção não eliminada. Aplicar a estratégia correspondente, i.e., construir uma prova de $\forall \meta{x}\, \atom{\meta{A}}{\meta{x}}$ no sentido contrário, é escrever $\atom{\meta{A}}{\meta{c}}$ acima dele e então continuar tentando encontrar uma prova daquela sentença.

\begin{proof}
	\ellipsesline
	\have[n]{n}{\atom{\meta{A}}{\meta{c}}}
	\have{m}{\forall \meta{x}\, \atom{\meta{A}}{\meta{x}}}\Ai{n}
\end{proof}
%$\atom{\meta{A}}{\meta{c}}$ is obtained from $\atom{\meta{A}}{\meta{x}}$ by replacing every free occurrence of $\meta{x}$ in $\atom{\meta{A}}{\meta{x}}$ by~$\meta{c}$. For this to work, $\meta{c}$ must satisfy the special condition. We can ensure that it does by always picking a name that does not already occur in the proof constructed so far. (Of course, it will occur in the proof we end up constructing---just not in an assumption that is undischarged at line~$n+1$.)
%
$\atom{\meta{A}}{\meta{c}}$ é obtido de $\atom{\meta{A}}{\meta{x}}$ ao substituir toda ocorrência livre de $\meta{x}$ em $\atom{\meta{A}}{\meta{x}}$ por~$\meta{c}$. Para esse trabalho, $\meta{c}$ deve satisfazer a condição especial. Nós garantimos que ela satisfaz ao sempre escolhermos um nome que ainda não ocorre na prova construída até então. (Certamente, ele ocorrerá na prova que acabarmos construindo---apenas não em uma assunção que não eliminada naquela linha~$n+1$.)

%To work backward from a sentence $\exists \meta{x}\, \atom{\meta{A}}{\meta{x}}$ we similarly write a sentence above it that can serve as a justification for an application of the $\exists$I rule, i.e., a sentence of the form $\atom{\meta{A}}{\meta{c}}$. 
Para trabalhar de trás para frente a partir de uma sentença $\exists \meta{x}\, \atom{\meta{A}}{\meta{x}}$, nós simplesmente escrevemos uma sentença sobre ela que sirva como uma justificação para uma aplicação da regra $\exists$I, i.e., uma sentença da forma $\atom{\meta{A}}{\meta{c}}$. 

\begin{proof}
	\ellipsesline
	\have[n]{n}{\atom{\meta{A}}{\meta{c}}}
	\have{m}{\exists \meta{x}\, \atom{\meta{A}}{\meta{x}}}\Ei{n}
\end{proof}
%This looks just like what we would do if we were working backward from a universally quantified sentence. The difference is that whereas for $\forall$I we have to pick a name~$\meta{c}$ which does not occur in the proof (so far), for $\exists$I we may and in general must pick a name~$\meta{c}$ which already occurs in the proof.  Just like in the case of $\eor$I, it is often not clear which $\meta{c}$ will work out, and so to avoid having to backtrack you should work backward from existentially quantified sentences only when all other strategies have been applied.
%
Isso parece com o que faríamos caso trabalhássemos no sentido contrário a partir de uma sentença quantificada universalmente. A diferença é que enquanto para $\forall$I nós temos que escolher um nome~$\meta{c}$ que não ocorre na prova (até então, para $\exists$I nós podemos, e em geral devemos, escolher um nome~$\meta{c}$ que já ocorreu na prova. Assim como no caso de $\eor$I, frequentemente não é claro qual $\meta{c}$ vai dar certo, e, então, para evitar ter que retroceder, você deve trabalhar de trás para frente a partir de sentenças quantificadas existencialmente apenas quando todas as outras estratégias tiverem sido aplicadas.

%By contrast, working \emph{forward} from sentences $\exists \meta{x}\, \atom{\meta{A}(\meta{x}})$ generally always works and you won't have to backtrack. Working forward from an existentially quantified sentence takes into account not just $\exists \meta{x}\, \atom{\meta{A}}{\meta{x}}$ but also whatever sentence $\meta{B}$ you would like to prove. It requires that you set up a subproof above $\meta{B}$, wherein $\meta{B}$ is the last line, and a substitution instance $\atom{\meta{A}}{\meta{c}}$ of $\exists \meta{x}\, \atom{\meta{A}}{\meta{x}}$ as the assumption.  In order to ensure that the condition on $\meta{c}$ that governs $\exists$E is satisfied, chose a name $\meta{c}$ which does not already occur in the proof. 
%
Por outro lado, trabalhar \emph{a partir de} de sentenças $\exists \meta{x}\, \atom{\meta{A}(\meta{x}})$ geralmente funcionam sempre e você não precisará retroceder. Trabalhar a partir de uma sentença existencialemnte quantificada leva e, conta não apenas $\exists \meta{x}\, \atom{\meta{A}}{\meta{x}}$, mas também qualquer sentença $\meta{B}$ que você gostaria de provar. Isso requer que você estabeleça uma subprova sobre $\meta{B}$, em que $\meta{B}$ é a última linha, e uma instância de substituição $\atom{\meta{A}}{\meta{c}}$ de $\exists \meta{x}\, \atom{\meta{A}}{\meta{x}}$ é a assunção. Para garantir que a condição em $\meta{c}$ que governa $\exists$E é satisfeita, escolha um nome $\meta{c}$ que ainda não ocorreu na prova.
\begin{proof}
	\ellipsesline
	\have[m]{m}{\exists \meta{x}\, \atom{\meta{A}}{\meta{x}}}
	\ellipsesline
	\open
	\hypo[n]{n}{\atom{\meta{A}}{\meta{c}}}
	\ellipsesline
	\have[k]{k}{\meta{B}}
	\close
	\have{e}{\meta{B}}\Ee{m,n-k}
\end{proof}
%You'll then continue with the goal of proving $\meta{B}$, but now inside a subproof in which you have an additional sentence to work with, namely~$\atom{\meta{A}}{\meta{c}}$.
Então, você continuará com a meta de provar $\meta{B}$, mas, agora, dentro de uma subprova em que você tem uma sentença adicional para trabalhar, a saber,~$\atom{\meta{A}}{\meta{c}}$.

%Lastly, working forward from $\forall \meta{x}\, \atom{\meta{A}}{\meta{x}}$ means that you can always write down $\atom{\meta{A}}{\meta{c}}$ and justify it using $\forall$E, for any name~$\meta{c}$. Of course, you wouldn't want to do that willy-nilly. Only certain names $\meta{c}$ will help in your task of proving whatever goal sentence you are working on. So, like working backward from $\exists \meta{x}\, \atom{\meta{A}}{\meta{x}}$, you should work forward from $\forall \meta{x}\, \atom{\meta{A}}{\meta{x}}$ only after all other strategies have been applied.
%
Por último, trabalhar a partir de $\forall \meta{x}\, \atom{\meta{A}}{\meta{x}}$ significa que você pode sempre escrever $\atom{\meta{A}}{\meta{c}}$ e justificá-lo usando $\forall$E, para qualquer nome~$\meta{c}$. Certamente, você não iria querer fazer isso à vontade. Apenas certos nomes $\meta{c}$ ajudarão em sua tarefa de provar qualquer que seja a sentença na qual você está trabalhando. Então, assim como trabalhar no sentido contrário a partir de $\exists \meta{x}\, \atom{\meta{A}}{\meta{x}}$, você deveria avançar a partir de $\forall \meta{x}\, \atom{\meta{A}}{\meta{x}}$ apenas depois de todas as outras estratégias terem sido aplicadas.

%Let's consider as an example the argument $\forall x(\atom{A}{x} \eif B) \therefore \exists x\,\atom{A}{x} \eif B$. To start constructing a proof, we write the premise at the top and the conclusion at the bottom.
Vamos considerar aqui um exemplo do argumento $\forall x(\atom{A}{x} \eif B) \therefore \exists x\,\atom{A}{x} \eif B$. Para começar a construir uma prova, escrevemos a premissa no topo e a conclusão no fim.
\begin{proof}
\hypo{1}{\forall x(\atom{A}{x} \eif B)}
\ellipsesline
\have[n]{7}{\exists x\,\atom{A}{x} \eif B}
\end{proof}
%The strategies for connectives of TFL still apply, and you should apply them in the same order: first work backward from conditionals, negated sentences, conjunctions, and now also universal quantifiers, then forward from disjunctions and now existential quantifiers, and only then try to apply $\eif$E, $\enot$E, $\lor$I, $\forall$E, or $\exists$I. In our case, that means, working backward from the conclusion:
As estratégias para conectivos da LVF continuam se aplicando, e você deve aplicá-las na mesma ordem: primeiro trabalhe no sentido contrário a partir de condicionais, sentenças engadas, conjunções e agora também quantificadores universais, e então para frente a partir de disjunções e quantificadores existenciais, e apenas então tente aplicar $\eif$E, $\enot$E, $\lor$I, $\forall$E, or $\exists$I. En nosso caso, isso significa trabalhar no sentido contrário a partir da conclusão:

\begin{proof}
	\hypo{1}{\forall x(\atom{A}{x} \eif B)}
	\open
	\hypo{2}{\exists x\,\atom{A}{x}}
	\ellipsesline
	\have[n][-1]{6}{B}
	\close
	\have[n]{7}{\exists x\,\atom{A}{x} \eif B}\ci{2-(6)}
\end{proof}
%Our next step should be to work forward from $\exists x\,\atom{A}{x}$ on line~$2$. For that, we have to pick a name not already in our proof. Since no names appear, we can pick any name, say~`$d$'
%
Nosso próximo passo deve ser avançar a partir $\exists x\,\atom{A}{x}$ on line~$2$. Para isso, temos que escolher um nome que ainda não esteja em nossa prova. Uma vez que nenhum nome aparece, podemos escolher qualquer nome, digamos,~`$d$'.
\begin{proof}
	\hypo{1}{\forall x(\atom{A}{x} \eif B)}
	\open
	\hypo{2}{\exists x\,\atom{A}{x}}
	\open
	\hypo{3}{\atom{A}{d}}
	\ellipsesline
	\have[n][-2]{5}{B}
	\close
	\have[n][-1]{6}{B}\Ee{2,3-(5)}
	\close
	\have[n]{7}{\exists x\,\atom{A}{x} \eif B}\ci{2-(6)}
\end{proof}
%Now we've exhausted our primary strategies, and it is time to work forward from the premise $\forall x(\atom{A}{x} \eif B)$. Applying $\forall$E means we can justify any instance of $A(\meta{c}) \eif B$, regardless of what $\meta{c}$ we choose. Of course, we'll do well to choose $d$, since that will give us $\atom{A}{d} \eif B$. Then we can apply $\eif$E to justify~$B$, finishing the proof.
%
Agora esgotamos nossas estratégias primárias e é hora de avançar a partir da premissa $\forall x(\atom{A}{x} \eif B)$. Aplicar $\forall$E significa que podemos justificar qualquer instância de $A(\meta{c}) \eif B$, independentemente de qual $\meta{c}$ escolhermos. É claro, fazemos bem em escolher $d$, uma vez que isso nos dará $\atom{A}{d} \eif B$. Podemos, então, aplicar $\eif$E to justify~$B$,  finalizando a prova.
\begin{proof}
	\hypo{1}{\forall x(\atom{A}{x} \eif B)}
	\open
	\hypo{2}{\exists x\,\atom{A}{x}}
	\open
	\hypo{3}{\atom{A}{d}}
\have{4}{\atom{A}{d} \eif B}\Ae{1}
	\have{5}{B}\ce{4,3}
	\close
	\have{6}{B}\Ee{2,3-5}
	\close
	\have{7}{\exists x\,\atom{A}{x} \eif B}\ci{2-6}
\end{proof}

%Now let's construct a proof of the converse. We begin with
Vamos começar a construir uma prova do inverso. Começamos com
\begin{proof}
	\hypo{1}{\exists x\,\atom{A}{x} \eif B}
	\ellipsesline
	\have[n]{7}{\forall x(\atom{A}{x} \eif B)}
\end{proof}
%Note that the premise is a conditional, not an existentially quantified sentence, so we should not (yet) work forward from it. Working backward from the conclusion, $\forall x(\atom{A}{x} \eif B)$, leads us to look for a proof of $\atom{A}{d} \eif B$:
%
Note que a premissa é um condicional, não uma sentença quantificada existencialmente, então não devemos (ainda) avançar a partir dela. Trabalhar de trás para frente a partir da conclusão, $\forall x(\atom{A}{x} \eif B)$, nos leva a uma prova de $\atom{A}{d} \eif B$:
\begin{proof}
	\hypo{1}{\exists x\,\atom{A}{x} \eif B}
	\ellipsesline
	\have[n][-1]{6}{\atom{A}{d} \eif B}
	\have[n]{7}{\forall x(\atom{A}{x} \eif B)}\Ai{6}
\end{proof}
%And working backward from $\atom{A}{d} \eif B$ means we should set up a subproof with $\atom{A}{d}$ as an assumption and $B$ as the last line:
E trabalhar de trás para frente a partir de $\atom{A}{d} \eif B$ significa que deveríamos estabelecer uma subprova com $\atom{A}{d}$ como assunção e $B$ como última linha:
\begin{proof}
	\hypo{1}{\exists x\,\atom{A}{x} \eif B}
	\open
	\hypo{2}{\atom{A}{d}}
	\ellipsesline
	\have[n][-2]{5}{B}
	\close
	\have[n][-1]{6}{\atom{A}{d} \eif B}\ci{2-(5)}
	\have[n]{7}{\forall x(\atom{A}{x} \eif B)}\Ai{6}
\end{proof}
%Now we can work forward from the premise on line~$1$. That's a conditional, and its consequent happens to be the sentence~$B$ we are trying to justify. So we should look for a proof of its antecedent, $\exists x\,\atom{A}{x}$. Of course, that is now readily available, by $\exists$I from line~$2$, and we're done:
%
Agora, podemos avançar a partir da premissa da linha~$1$. Ela é um condicional, e seu consequente é a sentença~$B$ que estamos tentando justificar. Então, devemos procurar por uma prova do seu antecedente, $\exists x\,\atom{A}{x}$. Certamente, isso está agora prontamente disponível, por $\exists$I da linha~$2$, e nós terminamos:
\begin{proof}
	\hypo{1}{\exists x\,\atom{A}{x} \eif B}
	\open
	\hypo{2}{\atom{A}{d}}
	\have{3}{\exists x\,\atom{A}{x}}\Ei{2}
	\have{5}{B}\ce{1,3}
	\close
	\have{6}{\atom{A}{d} \eif B}\ci{2-5}
	\have{7}{\forall x(\atom{A}{x} \eif B)}\Ai{6}
\end{proof}

\practiceproblems

\problempart
%Use the strategies to find proofs for each of the following arguments and theorems:
Use as estratégias para encontrar provas para cada um dos seguintes argumentos e teoremas:
\begin{earg}
\item $A \eif \forall x\,\atom{B}{x} \therefore \forall x(A \eif \atom{B}{x})$
\item $\exists x(A \eif \atom{B}{x}) \therefore A \eif \exists x\, \atom{B}{x}$
\item $\forall x(\atom{A}{x} \eand \atom{B}{x}) \eiff (\forall x\,\atom{A}{x} \eand \forall x\,\atom{B}{x})$
\item $\exists x(\atom{A}{x} \eor \atom{B}{x}) \eiff (\exists x\,\atom{A}{x} \eor \exists x\,\atom{B}{x})$
\item $A \eor \forall x\,\atom{B}{x}) \therefore \forall x(A \eor \atom{B}{x})$
\item $\forall x(\atom{A}{x} \eif B) \therefore \exists x\,\atom{A}{x} \eif B$
\item $\exists x(\atom{A}{x} \eif B) \therefore \forall x\,\atom{A}{x} \eif B$
\item $\forall x(\atom{A}{x} \eif \exists y\,\atom{A}{y})$
\end{earg}
%Use only the basic rules of TFL in addition to the basic quantifier rules.
Use apenas as regras básicas da LVF somadas às regras básicas de quantificadoes.

\problempart
%Use the strategies to find proofs for each of the following arguments and theorems:
Use as estratégias para encontrar provas para cada um dos argumentos e teoremas:
\begin{earg}
\item $\forall x\,\atom{R}{x,x} \therefore \forall x\,\exists y\,\atom{R}{x,y}$
\item $\forall x\,\forall y\,\forall z[(\atom{R}{x,y} \eand \atom{R}{y,z}) \eif \atom{R}{x,z}]$ \\
$\therefore \forall x\,\forall y[\atom{R}{x,y} \eif \forall z(\atom{R}{y,z} \eif \atom{R}{x,z})]$
\item $\forall x\,\forall y\,\forall z[(\atom{R}{x,y} \eand \atom{R}{y,z}) \eif \atom{R}{x,z}],$\\ $\forall x\,\forall y(\atom{R}{x,y} \eif \atom{R}{y, x})$ \\ $\therefore \forall x\,\forall y\,\forall z[(\atom{R}{x,y} \eand \atom{R}{x,z}) \eif \atom{R}{y,z}]$
\item $\forall x\,\forall y(\atom{R}{x,y} \eif \atom{R}{y, x})$ \\$\therefore \forall x\,\forall y\,\forall z[(\atom{R}{x,y} \eand \atom{R}{x,z}) \eif \exists u(\atom{R}{y,u} \eand \atom{R}{z,u})]$
\item $\enot \exists x\,\forall y (\atom{A}{x, y} \eiff \lnot\atom{A}{y, y})$
\end{earg}

\problempart
%Use the strategies to find proofs for each of the following arguments and theorems:
Use as estratégias para encontrar provas para cada um dos argumentos e teoremas:
\begin{earg}
\item $\forall x\,\atom{A}{x} \eif B \therefore \exists x(\atom{A}{x} \eif B)$
\item $A \eif \exists x\, \atom{B}{x} \therefore \exists x(A \eif \atom{B}{x})$
\item $\forall x(A \eor \atom{B}{x}) \therefore A \eor \forall x\,\atom{B}{x})$
\item $\exists x(\atom{A}{x} \eif \forall y\,\atom{A}{y})$
\item $\exists x(\exists y\,\atom{A}{y} \eif \atom{A}{x})$
\end{earg}
%These require the use of IP. Use only the basic rules of TFL in addition to the basic quantifier rules.
Essas requerem o uso de IP. Use apenas as regras básicas da LVF somadas às regras básicas de quantificadoes. %o que é IP?

\chapter{Conversão de quantificadores}\label{s:CQ}%\chapter{Conversion of quantifiers}\label{s:CQ}

%In this section, we will add some additional rules to the basic rules of the previous section. These govern the interaction of quantifiers and negation.
Nesta seção, adicionaremos algumas regras adicionais às regras básicas da seção anterior. Elas governam a interação entre quantificadores e a negação.
 
%In \S\ref{s:FOLBuildingBlocks}, we noted that $\enot\exists x\meta{A}$ is logically equivalent to $\forall x\, \enot\meta{A}$. We will add some rules to our proof system that govern this. In particular, we add:
Em \S\ref{s:FOLBuildingBlocks}, notamos que $\enot\exists x\meta{A}$ é logicamente equivalente a $\forall x\, \enot\meta{A}$. Adicionaremos algumas regras ao nosso sistema de prova que governam isso. Em particular, adicionamos:
	\factoidbox{
	\begin{proof}
		\have[m]{a}{\forall \meta{x}\, \enot\meta{A}}
		\have[\ ]{con}{\enot \exists \meta{x}\, \meta{A}}\cq{a}
	\end{proof}}
e%and
\factoidbox{
	\begin{proof}
		\have[m]{a}{ \enot \exists \meta{x}\, \meta{A}}
		\have[\ ]{con}{\forall \meta{x}\, \enot \meta{A}}\cq{a}
	\end{proof}}
Igualmente, adicionamos:%Equally, we add:
\factoidbox{
	\begin{proof}
		\have[m]{a}{\exists \meta{x}\, \enot \meta{A}}
		\have[\ ]{con}{\enot \forall \meta{x}\, \meta{A}}\cq{a}
	\end{proof}}
e%and
\factoidbox{
	\begin{proof}
		\have[m]{a}{\enot \forall \meta{x}\, \meta{A}}
		\have[\ ]{con}{\exists \meta{x}\, \enot \meta{A}}\cq{a}
	\end{proof}}

\practiceproblems
\problempart
%Show in each case that the sentences are provably inconsistent:
Mostre em cada caso que as sentenças são demonstravelmente inconsistentes:
\begin{earg}
\item $\atom{S}{a}\eif \atom{T}{m}, \atom{T}{m} \eif \atom{S}{a}, \atom{T}{m} \eand \enot \atom{S}{a}$
\item $\enot\exists x\,\atom{R}{x,a}, \forall x\, \forall y\,\atom{R}{y,x}$
\item $\enot\exists x\, \exists y\,\atom{L}{x,y}, \atom{L}{a,a}$
\item $\forall x(\atom{P}{x} \eif \atom{Q}{x}), \forall z(\atom{P}{z} \eif \atom{R}{z}), \forall y\,\atom{P}{y}, \enot \atom{Q}{a} \eand \enot \atom{R}{b}$
\end{earg}

\problempart
Mostre em cada caso que cada par de sentença é demonstravelmente equivalente:%Show that each pair of sentences is provably equivalent:
\begin{earg}
\item $\forall x (\atom{A}{x}\eif \enot \atom{B}{x}), \enot\exists x(\atom{A}{x} \eand \atom{B}{x})$
\item $\forall x (\enot\atom{A}{x}\eif \atom{B}{d}), \forall x\,\atom{A}{x} \eor \atom{B}{d}$
\end{earg}

\problempart
%In \S\ref{s:MoreMonadic}, we considered what happens when we move quantifiers `across' various logical operators. Show that each pair of sentences is provably equivalent:
Em \S\ref{s:MoreMonadic}, consideramos o que ocorre quando movemos os quantificadores `entre' operadores lógicos. Mostr que cada par de sentenças é demonstravelmente equivalente:
\begin{earg}
\item $\forall x(\atom{F}{x} \eand \atom{G}{a}), \forall x\,\atom{F}{x} \eand \atom{G}{a}$
\item $\exists x(\atom{F}{x} \eor \atom{G}{a}), \exists x\,\atom{F}{x} \eor \atom{G}{a}$
\item $\forall x(\atom{G}{a} \eif \atom{F}{x}), \atom{G}{a} \eif \forall x\,\atom{F}{x}$
\item $\forall x(\atom{F}{x} \eif \atom{G}{a}), \exists x\,\atom{F}{x} \eif \atom{G}{a}$
\item $\exists x(\atom{G}{a} \eif \atom{F}{x}), \atom{G}{a} \eif \exists x\,\atom{F}{x}$
\item $\exists x(\atom{F}{x} \eif \atom{G}{a}), \forall x\,\atom{F}{x} \eif \atom{G}{a}$
\end{earg}
%NB: the variable `$x$' does not occur in `$\atom{G}{a}$'. When all the quantifiers occur at the beginning of a sentence, that sentence is said to be in \emph{prenex normal form}. These equivalences are sometimes called \emph{prenexing rules}, since they give us a means for putting any sentence into prenex normal form.
%
Nota: a variável `$x$' não ocorre em `$\atom{G}{a}$'. Quando todos os quantificadores ocorrem no começo de uma sentença, essa sentença é dita estar em sua \emph{forma normal prenex}. Essas equivalências são às vezes chamadas de \emph{regras prenex}, uma vez que elas nos dão meios de colocar qualquer sentença em sua forma normal prenex.

\chapter{Regras para identidade}%\chapter{Rules for identity}
%In \S\ref{s:Interpretations}, we mentioned the philosophically contentious thesis of the \emph{identity of indiscernibles}. This is the claim that objects which are indiscernible in every way are, in fact, identical to each other. It was also mentioned that we will not subscribe to this thesis. It follows that, no matter how much you learn about two objects, we cannot prove that they are identical. That is unless, of course, you learn that the two objects are, in fact, identical, but then the proof will hardly be very illuminating.
Em \S\ref{s:Interpretations}, mencionamos a tese filosoficamente controversa da \emph{identidade dos indiscerníveis}. Esta é a afirmação de que os objetos que são indiscerníveis em todos os sentidos são, de fato, idênticos entre si. Também foi mencionado que não admitiremos esta tese. Daqui se segue que, não importa o quanto você aprenda sobre dois objetos, não podemos provar que eles são idênticos. A menos que, é claro, você aprenda que os dois objetos são de fato idênticos, mas a prova dificilmente será muito esclarecedora.

%The general point, though, is that \emph{no sentences} which do not already contain the identity predicate could justify an inference to `$a=b$'. So our identity introduction rule cannot allow us to infer to an identity claim containing two \emph{different} names.
O ponto geral, porém, é que \emph{nenhuma sentença} que já não contenha o predicado de identidade pode justificar a inferência a `$a=b$'. Então, nossa regra de introdução da identidade não pode nos permitir inferir uma afirmação de identidade contendo dois nomes \emph{diferentes}.

%However, every object is identical to itself. No premises, then, are required in order to conclude that something is identical to itself. So this will be the identity introduction rule:
Contudo, todo objeto é idêntico a si mesmo. Nenhuma premissa, então, é requerida para concluir que algo é idêntico a si mesmo. Então, essa será a regra da introdução da identidade:
\factoidbox{
\begin{proof}
	\have[\ \,\,\,]{x}{\meta{c}=\meta{c}} \by{=I}{}
\end{proof}}
%Notice that this rule does not require referring to any prior lines of the proof. For any name \meta{c}, you can write $\meta{c}=\meta{c}$ on any point, with only the {=}I rule as justification. 
Note que esta regra não requer referência a quaisquer linhas anteriores da prova. Para qualquer nome \meta{c}, você pode escrever $\meta{c}=\meta{c}$ em qualquer ponto, apenas com a regra {=}I como justificação.

%Our elimination rule is more fun. If you have established `$a=b$', then anything that is true of the object named by `$a$' must also be true of the object named by `$b$'. For any sentence with `$a$' in it, you can replace some or all of the occurrences of `$a$' with `$b$' and produce an equivalent sentence. For example, from `$\atom{R}{a,a}$' and `$a = b$', you are justified in inferring `$\atom{R}{a,b}$', `$\atom{R}{b,a}$' or `$\atom{R}{b,b}$'. More generally:
Nossa regra de eliminação é mais legal. Se você estabeleceu `$a=b$', então qualquer coisa que for verdadeira sobre objeto nomeado por `$a$' também tem que ser verdadeira sobre o objeto nomeado por `$b$'. Para qualquer sentença com `$a$' nela, você pode subsituir alguma ou todas as ocorrências de `$a$' por `$b$' e produzir uma sentença equivalente. Por exemplo, a partir de `$\atom{R}{a,a}$' e `$a = b$', você está justificado a inferir `$\atom{R}{a,b}$', `$\atom{R}{b,a}$' ou `$\atom{R}{b,b}$'. De maneira mais geral:
\factoidbox{\begin{proof}
	\have[m]{e}{\meta{a}=\meta{b}}
	\have[n]{a}{\meta{A}(\ldots \meta{a} \ldots \meta{a}\ldots)}
	\have[\ ]{ea1}{\meta{A}(\ldots \meta{b} \ldots \meta{a}\ldots)} \by{=E}{e,a}
\end{proof}}
%The notation here is as for $\exists$I. So $\meta{A}(\ldots \meta{a} \ldots \meta{a}\ldots)$ is a formula containing the name $\meta{a}$, and $\meta{A}(\ldots \meta{b} \ldots \meta{a}\ldots)$ is a formula obtained by replacing one or more instances of the name $\meta{a}$ with the name $\meta{b}$. Lines $m$ and $n$ can occur in either order, and do not need to be adjacent, but we always cite the statement of identity first. Symmetrically, we allow:
A notação aqui é para $\exists$I. Então $\meta{A}(\ldots \meta{a} \ldots \meta{a}\ldots)$ é uma fórmula contendo o nome $\meta{a}$, e $\meta{A}(\ldots \meta{b} \ldots \meta{a}\ldots)$ é uma fórmula obtida ao substituir uma ou mais instâncias do nome $\meta{a}$ pelo nome $\meta{b}$. Linhas $m$ e $n$ podem ocorrer em qualquer ordem, e não precisam estar perto, mas sempre citaremos o enunciado de identidade primeiro. Simetricamente, nós permitimos:
\factoidbox{\begin{proof}
	\have[m]{e}{\meta{a}=\meta{b}}
	\have[n]{a}{\meta{A}(\ldots \meta{b} \ldots \meta{b}\ldots)}
	\have[\ ]{ea2}{\meta{A}(\ldots \meta{a} \ldots \meta{b}\ldots)} \by{=E}{e,a}
\end{proof}}
%This rule is sometimes called \emph{Leibniz's Law}, after Gottfried Leibniz. 
Esta regra é às vezes chamada de \emph{lei de Leibniz}, depois de Gottfried Leibniz.

%To see the rules in action, we will prove some quick results. First, we will prove that identity is \emph{symmetric}:
Para ver as regras em ação, provaremos alguns resultados rápidos. Primeiro, provaremos que a identidade é \emph{simétrica}:
\begin{proof}
	\open
		\hypo{ab}{a = b}
		\have{aa}{a = a}\by{=I}{}
		\have{ba}{b = a}\by{=E}{ab, aa}
	\close
	\have{abba}{a = b \eif b =a}\ci{ab-ba}
	\have{ayya}{\forall y (a = y \eif y = a)}\Ai{abba}
	\have{xyyx}{\forall x\, \forall y (x = y \eif y = x)}\Ai{ayya}
\end{proof}
%We obtain line 3 by replacing one instance of `$a$' in line 2 with an instance of `$b$'; this is justified given `$a= b$'. 
Obtemos a linha 3 ao substituir uma instância de `$a$' na linha 2 por uma instância de `$b$'; isso é justificado dado que `$a=b$'.

%Second, we will prove that identity is \emph{transitive}:
Segundo, provaremos que a identidade é \emph{transitiva}:
\begin{proof}
	\open
		\hypo{abc}{a = b \eand b = c}
		\have{ab}{a = b}\ae{abc}
		\have{bc}{b = c}\ae{abc}
		\have{ac}{a = c}\by{=E}{ab, bc}
	\close
	\have{con}{(a = b \eand b =c) \eif a = c}\ci{abc-ac}
	\have{conz}{\forall z((a = b \eand b = z) \eif a = z)}\Ai{con}
	\have{cony}{\forall y\,\forall z((a = y \eand y = z) \eif a = z)}\Ai{conz}
	\have{conx}{\forall x\,\forall y \forall z((x = y \eand y = z) \eif x = z)}\Ai{cony}
\end{proof}
%We obtain line 4 by replacing `$b$' in line 3 with `$a$'; this is justified given `$a= b$'. 
Obtemos a linha 4 ao substituir `$b$' na linha 3 por `$a$'; isso é justificado dado que `$a=b$'.

\practiceproblems
\problempart
\label{pr.identity}
Forneça uma prova de cada afirmação.%Provide a proof of each claim.
\begin{earg}
\item $\atom{P}{a} \eor \atom{Q}{b}, \atom{Q}{b} \eif b=c, \enot\atom{P}{a} \proves \atom{Q}{c}$
\item $m=n \eor n=o, \atom{A}{n} \proves \atom{A}{m} \eor \atom{A}{o}$
\item $\forall x\ x=m, \atom{R}{m,a} \proves \exists x\,\atom{R}{x,x}$
\item $\forall x\,\forall y(\atom{R}{x,y} \eif x=y)\proves \atom{R}{a,b} \eif \atom{R}{b,a}$
\item $\enot \exists x\enot x = m \proves \forall x\,\forall y (\atom{P}{x} \eif \atom{P}{y})$
\item $\exists x\,\atom{J}{x}, \exists x\, \enot\atom{J}{x}\proves \exists x\, \exists y\, \enot x = y$
\item $\forall x(x=n \eiff \atom{M}{x}), \forall x(\atom{O}{x} \eor \enot \atom{M}{x})\proves \atom{O}{n}$
\item $\exists x\,\atom{D}{x}, \forall x(x=p \eiff \atom{D}{x})\proves \atom{D}{p}$
\item $\exists x\bigl[(\atom{K}{x} \eand \forall y(\atom{K}{y} \eif x=y)) \eand \atom{B}{x}\bigr], Kd\proves \atom{B}{d}$
\item $\proves \atom{P}{a} \eif \forall x(\atom{P}{x} \eor \enot x = a)$
\end{earg}

\problempart
%Show that the following are provably equivalent:
Mostre que as fórmulas a seguir são demonstravelmente equivalentes:
\begin{ebullet}
\item $\exists x \bigl([\atom{F}{x} \eand \forall y (\atom{F}{y} \eif x = y)] \eand x = n\bigr)$
\item $\atom{F}{n} \eand \forall y (\atom{F}{y} \eif n= y)$
\end{ebullet}
%And hence that both have a decent claim to symbolize the English sentence `Nick is the~$F$'.\\
E, consequentemente, que ambas têm uma reivindicação decente de simbolizar a sentença portuguesa `Nick é o~$F$'\\

\problempart
%In \S\ref{sec.identity}, we claimed that the following are logically equivalent symbolizations of the English sentence `there is exactly one $F$':
Em \S\ref{sec.identity}, afirmamos que as seguintes sentenças são simbolizações logicamente equivalentes da sentença portuguesa `há exatamente um $F$':
\begin{ebullet}
\item $\exists x\,\atom{F}{x} \eand \forall x\, \forall y \bigl[(\atom{F}{x} \eand \atom{F}{y}) \eif x = y\bigr]$
\item $\exists x \bigl[\atom{F}{x} \eand \forall y (\atom{F}{y} \eif x = y)\bigr]$
\item $\exists x\, \forall y (\atom{F}{y} \eiff x = y)$
\end{ebullet}
%Show that they are all provably equivalent. (\emph{Hint}: to show that three claims are provably equivalent, it suffices to show that the first proves the second, the second proves the third and the third proves the first; think about why.)
Mostre que elas são todas demonstravelmente equivalentes. (\emph{Dica}: para mostrar que as três sentenças são demonstravelmente equivalentes, é suficiente mostrar que a primeira prova a segunda, a segunda prova a primeira e a terceira prova a primeira; pense sobre o motivo disso).


\
\problempart
Simbolize o seguinte argumento%Symbolize the following argument
	\begin{quote}
		%There is exactly one $F$. There is exactly one $G$. Nothing is both $F$ and~$G$. So: there are exactly two things that are either~$F$ or~$G$.
		Há exatamente um $F$. Há exatamente um $G$. Nada é ao mesmo tempo $F$ e~$G$. Então: há exatamente duas coisas que são ou~$F$ ou~$G$.
	\end{quote}
E forneça uma prova disso.%And offer a proof of it.
%\begin{ebullet}
%\item  $\exists x \bigl[\atom{F}{x} \eand \forall y (\atom{F}{y} \eif x = y)\bigr], \exists x \bigl[\atom{G}{x} \eand \forall y (\atom{G}{y} \eif x = y)\bigr], \forall x (\enot\atom{F}{x} \eor \enot \atom{G}{x}) \proves \exists x\, \exists y \bigl[\enot x = y \eand \forall z ((\atom{F}{z} \eor \atom{G}{z}) \eif (x = y \eor x = z))\bigr]$
%\end{ebullet}




\chapter{Regras derivadas}\label{s:DerivedFOL}%\chapter{Derived rules}\label{s:DerivedFOL}
%As in the case of TFL, we first introduced some rules for FOL as basic (in \S\ref{s:BasicFOL}), and then added some further rules for conversion of quantifiers (in \S\ref{s:CQ}). In fact, the CQ rules should be regarded as \emph{derived} rules, for they can be derived from the  \emph{basic} rules of \S\ref{s:BasicFOL}. (The point here is as in \S\ref{s:Derived}.) Here is a justification for the first CQ rule:
Como nos casos da LVF, nós primeiro introduzimos algumas regras para a LPO como básicas (em \S\ref{s:BasicFOL}), e então adicionamos algumas outras regras para conversão de quantificadores (de agora em diante, CQ) em (in \S\ref{s:CQ}). De fato, as regras de CQ deveriam ser tratadas como regras \emph{derivadas} de \S\ref{s:BasicFOL}. (O ponto aqui é como em \S\ref{s:Derived}). Aqui está a justificação para a primeira regra de CQ:
\begin{proof}
	\hypo{An}{\forall x\, \enot \atom{A}{x}}
	\open
		\hypo{E}{\exists x\, \atom{A}{x}}
		\open
			\hypo{c}{\atom{A}{c}}%\by{for $\exists$E}{}
			\have{nc}{\enot \atom{A}{c}}\Ae{An}
			\have{red}{\ered}\ne{nc,c}
		\close
		\have{red2}{\ered}\Ee{E,c-red}
	\close
	\have{dada}{\enot \exists x\, \atom{A}{x}}\ni{E-red2}
\end{proof}
%You will note that on line 3 I have written `for $\exists$E'. This is not technically a part of the proof. It is just a reminder---to me and to you---of why I have bothered to introduce `$\enot \atom{A}{c}$' out of the blue. You might find it helpful to add similar annotations to assumptions when performing proofs. But do not add annotations on lines other than assumptions: the proof requires its own citation, and your annotations will clutter it.
Here is a justification of the third CQ rule:
\begin{proof}
	\hypo{nEna}{\exists x\, \enot \atom{A}{x}} 
	\open
		\hypo{Aa}{\forall x\, \atom{A}{x}}
		\open
			\hypo{nac}{\enot \atom{A}{c}}%\by{for $\exists$E}{}
			\have{a}{\atom{A}{c}}\Ae{Aa}
			\have{con}{\ered}\ne{nac,a}
		\close
		\have{con1}{\ered}\Ee{nEna, nac-con}
	\close
	\have{dada}{\enot \forall x\, \atom{A}{x}}\ni{Aa-con1}
\end{proof}
%This explains why the CQ rules can be treated as derived. Similar justifications can be offered for the other two CQ rules. 
Isso explica por que as regras de CQ podem ser tratadas como derivadas. Justificações similares podem ser ofereceidas para as outras duas regras CQ.

\practiceproblems

\problempart
%Offer proofs which justify the addition of the second and fourth CQ rules as derived rules.
Ofereça provas que justifiquem a adição da segunda e quarta regras de QC como regras derivadas.



\chapter{Prova e semântica}%\chapter{Proofs and semantics}
%We have used two different turnstiles in this book.  This:
Nós usamos duas diferentes catracas neste livro. Esta:
$$\meta{A}_1, \meta{A}_2, \ldots, \meta{A}_n \proves \meta{C}$$
%means that there is some proof which starts with assumptions $\meta{A}_1, \meta{A}_2, \ldots, \meta{A}_n$ and ends with $\meta{C}$ (and no undischarged assumptions other than $\meta{A}_1, \meta{A}_2, \ldots, \meta{A}_n$). This is a \emph{proof-theoretic notion}.
significa que há alguma prova que começa com as assunções $\meta{A}_1, \meta{A}_2, \ldots, \meta{A}_n$ e termina com $\meta{C}$ (e nenhuma assunção não eliminada além de $\meta{A}_1, \meta{A}_2, \ldots, \meta{A}_n$). Essa é uma \emph{noção prova-teórica [\textit{proof-theoretic}]}.

Por contraste, essa:%By contrast, this:
$$\meta{A}_1, \meta{A}_2, \ldots, \meta{A}_n \entails \meta{C}$$
significa que nenhuma valoração (ou interpretação) torna todas as fórmulas de $\meta{A}_1, \meta{A}_2, \ldots, \meta{A}_n$ verdadeiras e ~$\meta{C}$ falsa. Isso se trata de atribuições de verdade e falsidade a sentenças. É uma \emph{noção semântica}.

%It cannot be emphasized enough that these are different notions. But we can emphasize it a bit more: \emph{They are different notions.}
Não podemos enfatizar o suficiente que estas são noções diferentes. Mas podemos enfatizar um pouco mais: \emph{Essas são noções diferentes}

%Once you have internalised this point, continue reading. 
Uma vez que você tive internalizado este ponto, continue lendo.

%Although our semantic and proof-theoretic notions are different, there is a deep connection between them. To explain this connection,we will start by considering the relationship between validities and theorems.
Apesar de nossas noções semânticas de prova-teóricas [\textit{proof-theoretic}] serem diferentes, há uma profunda conexão entre elas. Para explicar esta conexão, começaremos considerando a relação entre tautologias e teoremas.

%To show that a sentence is a theorem, you need only produce a proof. Granted, it may be hard to produce a twenty line proof, but it is not so hard to check each line of the proof and confirm that it is legitimate; and if each line of the proof individually is legitimate, then the whole proof is legitimate. Showing that a sentence is a validity, though, requires reasoning about all possible interpretations. Given a choice between showing that a sentence is a theorem and showing that it is a validity, it would be easier to show that it is a theorem.
Para mostrar que uma sentença é um teorema, você só precisa produzir uma prova. Certamente, pode ser difícil produzir uma prova de vinte linhas, mas não é tão difícil verificar cada linha da prova e confirmar se ela é legítima; e se cada linha da prova individualmente é legítima, então toda a prova é legítima. Mostrar que uma sentença é uma tautologia, contudo, requer raciocinar sobre todas as interpretações possíveis. Dada uma escolha entre mostrar que uma sentença é um teorema e mostrar que é uma tautologia, seria mais fácil mostrar que é um teorema.

%Contrawise, to show that a sentence is \emph{not} a theorem is hard. We would need to reason about all (possible) proofs. That is very difficult. However, to show that a sentence is not a validity, you need only construct an interpretation in which the sentence is false. Granted, it may be hard to come up with the interpretation; but once you have done so, it is relatively straightforward to check what truth value it assigns to a sentence. Given a choice between showing that a sentence is not a theorem and showing that it is not a validity, it would be easier to show that it is not a validity.
Por outro lado, para mostrar que uma sentença \emph{não} é um teorema é difícil. Precisamos raciocinar sobre todas as provas (possíveis). Isso é muito difícil. No entanto, para mostrar que uma sentença não é uma tautologia, você precisa apenas construir uma interpretação na qual a sentença é falsa. Certamente, pode ser difícil apresentar a interpretação; mas uma vez feito isso, é relativamente simples verificar qual o valor de verdade que ela atribui a uma sentença. Dada uma escolha entre mostrar que uma sentença não é um teorema e mostrar que não é uma tautologia, seria mais fácil mostrar que não é uma tautologia.

%Fortunately, \emph{a sentence is a theorem if and only if it is a validity}. As a result, if we provide a proof of $\meta{A}$ on no assumptions, and thus show that $\meta{A}$ is a theorem,  i.e.\ ${}\proves \meta{A}$, we can legitimately infer that $\meta{A}$ is a validity, i.e., $\entails\meta{A}$. Similarly, if we construct an interpretation in which \meta{A} is false and thus show that it is not a validity, i.e.\ $\nentails \meta{A}$, it follows that \meta{A} is not a theorem, i.e.\  $\nproves \meta{A}$.
Felizmente, \emph{uma sentença é um teorema se e somente se ela for uma tautologia}. Como resultado, se fornecermos uma prova de $\meta{A}$ sem assunções, e então mostrarmos que $\meta{A}$ é um teorema, i.e.\ ${}\proves \meta{A}$, poderemos legitimamente inferir que $\meta{A}$ é uma tautologia, i.e., $\entails\meta{A}$. Similarmente, se construirmos uma interpretação em que \meta{A} é falsa e, consequentemente, mostrarmos que não é uma tautologia, i.e.\ $\nentails \meta{A}$, segue-se que \meta{A} não é um teorema, i.e.\  $\nproves \meta{A}$.

De maneira mais geral, temos os seguintes resultados poderosos:%More generally, we have the following powerful result:
$$\meta{A}_1, \meta{A}_2, \ldots, \meta{A}_n \proves\meta{B} \textbf{ iff }\meta{A}_1, \meta{A}_2, \ldots, \meta{A}_n \entails\meta{B}$$
%This shows that, whilst provability and entailment are \emph{different} notions, they are extensionally equivalent. As such:
Isso mostra que, enquanto a provabilidade [\textit{provability}] e o acarretamento [\textit{entailment}] são noções \emph{diferentes}, elas são extensionalmente equivalentes. Como tal:
	\begin{ebullet}
		%\item An argument is \emph{valid} iff \emph{the conclusion can be proved from the premises}.
		%\item Two sentences are \emph{logically equivalent} iff they are \emph{provably equivalent}.
		%\item Sentences are \emph{satisfiable} iff they are \emph{not provably inconsistent}.
		
		\item Um argumento é válido \emph{válido} sse \emph{a conclusão pode ser provada a partir das premissas}.
		\item Duas sentenças são \emph{logicamente equivalentes} sse elas são \emph{demonstravelmente equivalentes}.
		\item Sentenças são \emph{satisfatíveis} sse elas não são \emph{demonstravelmente inconsistentes}.
	\end{ebullet}
%For this reason, you can pick and choose when to think in terms of proofs and when to think in terms of valuations/interpretations, doing whichever is easier for a given task. The table on the next page summarises which is (usually) easier.
Por esse motivo, você pode escolher quando pensar em termos de provas e quando pensar em termos de valorações/interpretações, fazendo o que for mais fácil para uma determinada tarefa. A tabela na próxima página resume qual (geralmente) é mais fácil.

%It is intuitive that provability and semantic entailment should agree. But---let us repeat this---do not be fooled by the similarity of the symbols `$\entails$' and `$\proves$'. These two symbols have very different meanings. The fact that provability and semantic entailment agree is not an easy result to come by. 
É intuitivo que a demonstrabilidade e o acarretamento semântico devem concordar. Mas---vamos repetir isso---não deixe ser enganado pela similaridade dos símbolos `$\entails$' e `$\proves$'. Estes símbolos têm significados bem diferentes. O fato de que a demonstrabilidade e o acarretamento semântico concordarem não é um resultado fácil a se chegar.

%In fact, demonstrating that provability and semantic entailment agree is, very decisively, the point at which introductory logic becomes intermediate logic.
De fato, provar que demonstrabilidade e acarretamento semântico concordam é, de maneira bem decisível, o ponto em que a lógica introdutória se torna lógica intermediária.

\begin{sidewaystable}\small
\begin{center}
\begin{tabular*}{\textwidth}{p{.25\textheight}p{.325\textheight}p{.325\textheight}}
% & \textbf{Yes}  & \textbf{No}\\
 & \textbf{Sim}  & \textbf{Não}\\
\\
\meta{A} é uma \textbf{tautologia}? %Is \meta{A} a \textbf{validity}? 
%& give a proof which shows $\proves\meta{A}$ 
%& give an interpretation in which \meta{A} is false\\
& dê uma prova que mostra $\proves\meta{A}$ 
& dê uma interpretação em que \meta{A} é falso\\
\\
\meta{A} é uma \textbf{contradição}? &%Is \meta{A} a \textbf{contradiction}? &
%give a proof which shows $\proves\enot\meta{A}$ & 
%give an interpretation in which \meta{A} is true\\
dê uma prova que mostra $\proves\enot\meta{A}$ & 
dê uma interpretação em que \meta{A} é verdadeiro\\
\\
%Is \meta{A} contingent? & 
%give two interpretations, one in which \meta{A} is true and another in which \meta{A} is false & give a proof which either shows $\proves\meta{A}$ or $\proves\enot\meta{A}$\\
%\\
\meta{A} e \meta{B} são \textbf{equivalentes}? &%Are \meta{A} and \meta{B} \textbf{equivalent}? &
%give two proofs, one for $\meta{A}\proves\meta{B}$ and one for $\meta{B}\proves\meta{A}$  
%& give an interpretation in which \meta{A} and \meta{B} have different truth values\\
dê duas provas, uma para $\meta{A}\proves\meta{B}$ e uma para $\meta{B}\proves\meta{A}$  
& dê uma interpretação em que \meta{A} e \meta{B} têm valores de verdade diferentes\\
\\
$\meta{A}_1, \meta{A}_2, \ldots, \meta{A}_n$ são \textbf{conjuntamente satisfatíveis}? %Are $\meta{A}_1, \meta{A}_2, \ldots, \meta{A}_n$ \textbf{jointly satisfiable}? 
%& give an interpretation in which all of $\meta{A}_1, \meta{A}_2, \ldots, \meta{A}_n$ are true 
%& prove a contradiction from assumptions $\meta{A}_1, \meta{A}_2, \ldots, \meta{A}_n$\\
& dê uma interpretação em que todos de $\meta{A}_1, \meta{A}_2, \ldots, \meta{A}_n$ são verdadeiros
& prove uma contradição das assunções $\meta{A}_1, \meta{A}_2, \ldots, \meta{A}_n$\\
\\
$\meta{A}_1, \meta{A}_2, \ldots, \meta{A}_n \therefore \meta{C}$ é \textbf{válido}? %Is $\meta{A}_1, \meta{A}_2, \ldots, \meta{A}_n \therefore \meta{C}$ \textbf{valid}? 
%& give a proof with assumptions $\meta{A}_1, \meta{A}_2, \ldots, \meta{A}_n$ and concluding with \meta{C}
%& give an interpretation in which each of $\meta{A}_1, \meta{A}_2, \ldots, \meta{A}_n$ is true and \meta{C} is false\\
& dê uma prova com as assunções $\meta{A}_1, \meta{A}_2, \ldots, \meta{A}_n$ e conclusão \meta{C}
& dê uma interpretação em que cada um dos  $\meta{A}_1, \meta{A}_2, \ldots, \meta{A}_n$ é verdadeiro e \meta{C} é falso\\
\end{tabular*}
\end{center}
\end{sidewaystable}


